The present application relates generally to an improved data processing apparatus and method and more specifically to mechanisms for enhanced analysis of array-based netlists via phase abstraction.
Formal and semiformal verification techniques are powerful tools for the construction of correct logic designs. They have the power to expose even the most probabilistically uncommon scenario that may result in a functional design failure, and ultimately have the power to prove that the design is correct, i.e. that no failing scenario exists. Unfortunately, formal verification techniques require computational resources that are exponential with respect to the size of the design under test. Semiformal verification techniques leverage formal algorithms to larger designs by applying them only in a resource-bounded manner, though at the expense of incomplete verification coverage.
U.S. Pat. No. 6,698,003 proposes the generic concept of “transformation-based verification” to enable the use of multiple algorithms, encapsulated as “engines” of a modular multiple-engine based verification system to synergistically simplify and decompose complex problems into simpler sub-problems that are easier to formally discharge. The transformation-based verification paradigm has demonstrated itself essential to enhance the scalability of formal verification algorithms to verification problems of industrial relevance, where it is often desired to leverage the bug-hunting power of formal methods to large units of logic that are the common focus of simulation-based test benches.
One large capacity gap between traditional formal verification algorithms and simulation-based testbenches is due to bit-blasting employed in the former. In particular, virtually every industrial hardware formal verification tool “bit-blasts” design components into simpler primitives, such as two-input AND gates, inverters, and single-bit state elements. In contrast, logic simulators often support higher-level primitives without bit-blasting. One type of design component that often entails a dramatic bloat when bit-blasted is a memory array, which is a row-addressable, two-dimensional state element often used to represent main memory or caches. Such memory arrays may be extremely large when bit-blasted. Modern caches often are several megabytes, and if verifying a design component that interacts with main memory, it may even be required to support more than 232 rows of arbitrary width. Bit-blasting of such large memory arrays often constitutes a fatal bottleneck to formal verification tools.
Phase abstraction is a technique to reduce the size of a hardware design by unfolding the next-state functions of state-holding elements, such that one time-step/transition of the resulting phase-abstracted design correlates to multiple transitions of the original design. Phase abstraction is capable of reducing the number of state elements of a design, which is advantageous in enabling various verification and synthesis frameworks to be more efficient. However, no prior art solutions address the use of phase abstraction in a verification tool that natively supports memory arrays.